ImaginaryCTF Normal Write Up

Details:

Jeopardy style CTF

Category: Reverse Engineering

Points: 150

Comments: Norse senor snorts spores, abhors non-nors, adores s'mores, and snores.

Write up:

For this challenge I noticed that this would require a z3 script to solve so I went and wrote a script:

from z3 import *

s = Solver()

c1 = 31018867225649183750977872687351002051600286721243490293006893720934187569827

c2 = 95000751626272728732540896924058463535582995596703552905478832713420442258465

w1 = BitVec('w1', 256)
w2 = BitVec('w2', 256)
w3 = BitVec('w3', 256)
w4 = BitVec('w4', 256)
w5 = BitVec('w5', 256)
w6 = BitVec('w6', 256)
w7 = BitVec('w7', 256)
w8 = BitVec('w8', 256)
flag = BitVec('flag', 256)

s.add(0 == ~(w7 | w8))
s.add(w8 == ~(c2 | w6))
s.add(w7 == ~(w5 | w6))
s.add(w6 == ~(w5 | c2))
s.add(w5 == ~(w4 | w4))
s.add(w4 == ~(w2 | w3))
s.add(w3 == ~(c1 | w1))
s.add(w2 == ~(flag | w1))
s.add(w1 == ~(flag | c1))

print(s.check())
print(s.assertions())
print(s.model())

The script solves backwards from the output since we know that wrong equals 0. Once solved it then prints out the flag:

sat
[~(w7 | w8) == 0,
 w8 ==
 ~(95000751626272728732540896924058463535582995596703552905478832713420442258465 |
   w6),
 w7 == ~(w5 | w6),
 w6 ==
 ~(w5 |
   95000751626272728732540896924058463535582995596703552905478832713420442258465),
 w5 == ~(w4 | w4),
 w4 == ~(w2 | w3),
 w3 ==
 ~(31018867225649183750977872687351002051600286721243490293006893720934187569827 |
   w1),
 w2 == ~(flag | w1),
 w1 ==
 ~(flag |
   31018867225649183750977872687351002051600286721243490293006893720934187569827)]
[flag = 47668570326127048956762932830410417122100854461059692807700035289503302295933,
 w5 = 20791337611043466691030088084629444317686989068937011133978751294492687381470,
 w6 = 0,
 w1 = 66052701655906345724185538207492476107575919540020466922114743855448041016320,
 w4 = 95000751626272728732540896924058463535582995596703552905478832713420442258465,
 w3 = 18720520355760665948407574113844429694093778404376606824335946431530901053788,
 w2 = 2070817255282800742622513970785014623593210664560404309642804862961786327682,
 w7 = 95000751626272728732540896924058463535582995596703552905478832713420442258465,
 w8 = 20791337611043466691030088084629444317686989068937011133978751294492687381470]

I then converted the decimal flag value to hex:

0x696374667B4131315F686121315F7468335F6E33775F6E30726D5F6E3072217D

When run through a hex to ascii converted I then got:

ictf{A11_ha!1_th3_n3w_n0rm_n0r!}